package resolution;

import java.util.ArrayList;
import java.util.Enumeration;
import java.util.Hashtable;

import base.Atome;
import base.Constante;
import base.Et;
import base.Existe;
import base.Fonction;
import base.Formule;
import base.Non;
import base.OperateurBinaire;
import base.OperateurUnaire;
import base.Ou;
import base.PourTout;
import base.Quantification;
import base.Terme;
import base.Variable;

/**
 * Permet de réaliser le processus de résolution
 * 
 */
public class Resolution {

	public static int CHANGEMENT_RENOMMAGE_REMONTER_QUANTIF = 0;
	private Formule[] premisses;
	private Formule conclusion;
	private Formule nCcl;

	private Hashtable<Variable, Terme> substitutionToClause;
	private ArrayList<Formule> clauses;
	public int changement = 0;
	private int nbClauseCCl = 0;

	/**
	 * Constructeur exécutant le processus de résolution
	 * 
	 * @param premisses
	 * @param conclusion
	 */
	public Resolution(Formule[] premisses, Formule conclusion) {

		this.premisses = premisses;
		this.conclusion = conclusion;

		System.out.println("===> 1. MODELISATION");
		for (int i = 0; i < premisses.length; i++) {
			System.out.println("\t [Prémisse " + (i + 1) + "]         " + premisses[i]);
		}
		System.out.println("\t [Conclusion]         " + conclusion);

		negationCcl();

		System.out.println("\n===> 2. NEGATION DE LA CONCLUSION ");
		System.out.println("\t [Conclusion]         " + nCcl);

		prenexe();

		System.out.println("\n===> 3. FORME PRENEXE ");
		for (int i = 0; i < premisses.length; i++) {
			System.out.println("\t [Prémisse " + (i + 1) + "]         " + premisses[i]);
		}
		System.out.println("\t [Conclusion]         " + nCcl);

		skolem();

		System.out.println("\n===> 4. FORME DE SKOLEM ");
		for (int i = 0; i < premisses.length; i++) {
			System.out.println("\t [Prémisse " + (i + 1) + "]         " + premisses[i]);
		}
		System.out.println("\t [Conclusion]         " + nCcl);

		standard();

		System.out.println("\n===> 5. FORME STANDARD DE SKOLEM ");
		for (int i = 0; i < premisses.length; i++) {
			System.out.println("\t [Prémisse " + (i + 1) + "]         " + premisses[i]);
		}
		System.out.println("\t [Conclusion]         " + nCcl);

		clausale();

		System.out.println("\n===> 6. FORME CLAUSALE ");
		for (Formule clause : clauses) {
			System.out.println("\t [Clause " + (clauses.indexOf(clause) + 1) + "]         " + clause);
		}

		System.out.println("\n===> 7. RESOLUTION PAR UNIFICATION A L'AIDE D'UN ARBRE ");
		if (unification()) {
			System.out.println("LA PROPRIETE EST VRAIE");
		} else {
			System.out.println("LA PROPRIETE EST FAUSSE");
		}
	}

	/**
	 * Permet de calculer la négation de la conclusion
	 */
	public void negationCcl() {
		nCcl = conclusion.negation();
	}

	/**
	 * Met sous forme prénexe
	 */
	public void prenexe() {
		// descend les negations et retire les impliques aux premisses
		for (int i = 0; i < premisses.length; i++) {
			premisses[i] = premisses[i].enleveEquImp();
			premisses[i] = premisses[i].descendreNon();
		}

		// descend les négations et retire les impliques a la conclusion ( déjà
		// à
		// la forme négative)
		nCcl = nCcl.enleveEquImp();
		nCcl = nCcl.descendreNon();

		// prepare les formule a subir des rennomages et remonte les
		// quantificateurs des premisses
		for (int i = 0; i < premisses.length; i++) {
			premisses[i].renommer();
			premisses[i] = premisses[i].remonterQuantificateurs();
		}

		// renomme les variables de la conclusion
		nCcl.renommer();
		nCcl = nCcl.remonterQuantificateurs();
	}

	/**
	 * Met sous forme skolem
	 */
	public void skolem() {

		int nbSkol = 0;
		for (int i = 0; i < premisses.length; i++) {
			// ---------------------------------------------
			// ---------Mise en place des quantificateurs (existe - pour tout)
			// ---------------------------
			// pour chaque premisse si il y a un quantificateurs,
			if (premisses[i] instanceof Quantification) {
				Formule f = premisses[i];

				// si c'est un quantificateur existentiel on le passe
				while (f instanceof Existe) {
					f = ((Existe) f).getF();
				}

				while (f instanceof Quantification) {

					// si c'est un quantificateur absolu on le stocke et on voit
					// si il y a un existe apres

					if (f instanceof PourTout) {

						ArrayList<PourTout> aChanger = new ArrayList<PourTout>();
						Formule f2 = ((PourTout) f).getF();

						while (f2 instanceof PourTout) {
							aChanger.add((PourTout) f2);
							f2 = ((PourTout) f2).getF();
						}

						// si c'est un quantificateur existentiel on tombe sur
						// le cas pour tout puis existe
						if (f2 instanceof Existe) {

							Variable[] toChange = new Variable[aChanger.size()];
							for (int j = 0; j < aChanger.size(); j++) {
								toChange[i] = aChanger.get(i).getX();
							}
							// creation d'une focniton skolem
							Fonction foncSkolem = new Fonction("FonctSkol" + nbSkol, toChange);
							// substitution dans la premise
							premisses[i].substituer(((Quantification) f2).getX(), foncSkolem);
							Formule f3 = premisses[i];
							Formule f4 = premisses[i];
							// on enleve le il existe qui deviens inutile
							while (!((Quantification) f3).getX().equals(((Existe) f2).getX())) {
								f4 = f3;
								f3 = ((Quantification) f3).getF();
							}

							((Existe) f4).setF(((Quantification) f3).getF());

						}
					}

					f = ((Quantification) f).getF();
				}

			}

			if (nCcl instanceof Quantification) {

				Formule f = nCcl;

				while (f instanceof Existe) {
					f = ((Existe) f).getF();
				}

				while (f instanceof Quantification) {

					if (f instanceof PourTout) {

						ArrayList<PourTout> aChanger = new ArrayList<PourTout>();
						Formule f2 = ((PourTout) f).getF();

						while (f2 instanceof PourTout) {
							aChanger.add((PourTout) f2);
							f2 = ((PourTout) f2).getF();
						}

						if (f2 instanceof Existe) {
							Variable[] toChange = new Variable[aChanger.size()];

							for (int j = 0; j < aChanger.size(); j++) {
								toChange[i] = aChanger.get(i).getX();
							}

							Fonction foncSkolem = new Fonction("FonctSkol" + nbSkol, toChange);
							nCcl.substituer(((Quantification) f2).getX(), foncSkolem);
							Formule f3 = nCcl;
							Formule f4 = nCcl;

							while (!((Quantification) f3).getX().equals(((Existe) f2).getX())) {
								f4 = f3;
								f3 = ((Quantification) f3).getF();
							}

							((Existe) f4).setF(((Quantification) f3).getF());

						}
					}

					f = ((Quantification) f).getF();
				}

			}

		}

	}

	/**
	 * Met sous forme standard de skolem
	 */
	public void standard() {

		// on met les formules en conjonctive
		for (int i = 0; i < premisses.length; i++) {
			premisses[i] = premisses[i].toConjonctive();
		}

		nCcl = nCcl.toConjonctive();

	}

	/**
	 * Met sous forme clausale
	 */
	public void clausale() {

		// on fait des clauses
		clauses = new ArrayList<Formule>();

		nbClauseCCl = toClauses(nCcl, clauses.size()).size();
		clauses.addAll(toClauses(nCcl, clauses.size()));

		for (int i = 0; i < premisses.length; i++) {
			clauses.addAll(toClauses(premisses[i], clauses.size()));
		}

		// on renomme les clauses
		for (int i = 0; i < clauses.size(); i++) {

			Formule f = clauses.get(i);
			substitutionToClause = new Hashtable<Variable, Terme>();
			// on recherche les variables a renommer dans dans la formule dans
			// substitution toClause
			renommer(f);

			Enumeration<Variable> vars = substitutionToClause.keys();
			// on substitue dans tout f les variables a renommer
			while (vars.hasMoreElements()) {
				Variable var = vars.nextElement();
				f.substituer(var, substitutionToClause.get(var));
				clauses.set(i, f);
			}

		}
	}

	/**
	 * Permet de faire l'unification (phase finale du processus). Cette méthode
	 * permet de savoir si la propriété que l'on souhaite démontrer et vraie ou
	 * fausse
	 * 
	 * @return un boolean (true si propriété vraie sinon false)
	 */
	public boolean unification() {

		ArrayList<ArrayList<Formule>> ccl = new ArrayList<ArrayList<Formule>>();

		// reccupere tout sous array
		ArrayList<ArrayList<Formule>> toutesFormules = new ArrayList<ArrayList<Formule>>();
		for (Formule f : clauses) {
			toutesFormules.add(reccupererSousArray(f));
		}

		// on verifie que que pr chaque atome ou negation de chque clause on ait son contraire quelque part
		for (int i = 0; i < toutesFormules.size(); i++) {
			for (int j = 0; j < toutesFormules.get(i).size(); j++) {
				// on prende la negation
				Formule f = toutesFormules.get(i).get(j).negation();

				boolean contientnegation = false;
				for (int k = 0; k < toutesFormules.size(); k++) {
					if (k == i) {
						continue;
					}
					for (int l = 0; l < toutesFormules.get(k).size(); l++) {
						if (toutesFormules.get(k).get(l) instanceof Non && f instanceof Non) {
							if (((Atome) (((Non) toutesFormules.get(k).get(l)).getOperande())).isTheSame((Atome) ((Non) f).getOperande())) {
								contientnegation = true;
							}
						} else if (toutesFormules.get(k).get(l) instanceof Atome && f instanceof Atome) {
							if (((Atome) toutesFormules.get(k).get(l)).isTheSame((Atome) f)) {
								contientnegation = true;
							}
						}
					}
				}

				// si il ne contient pas, on suprrime des formules
				if (contientnegation == false) {
					toutesFormules.remove(i);
					// si on supprime un ccl, on change le nombre de ccl
					if (i < nbClauseCCl) {
						nbClauseCCl--;
					}
					break;
				}
			}
		}

		for (int i = 0; i < nbClauseCCl; i++) {
			ccl.add(toutesFormules.get(i));
		}
		ArrayList<Formule> ftemp = new ArrayList<Formule>();
		boolean ok = false;
		for (int i = 0; i < ccl.size(); i++) {

			ftemp.addAll(ccl.get(i));
			ArbreClause arbre = new ArbreClause(toutesFormules, ccl.get(i));
			if (arbre.resoudre()) {
				return true;
			}

		}
		return false;
	}

	public ArrayList<Formule> toClauses(Formule f1, int nbCst) {

		ArrayList<Formule> clauses = new ArrayList<Formule>();

		Formule f = f1;

		while (f instanceof Quantification) {
			// si c'est un existe on change la variable en constante
			if (f instanceof Existe) {
				Constante cons = new Constante("constClause" + nbCst);
				nbCst++;
				((Existe) f).getF().substituer(((Existe) f).getX(), cons);
			}
			f = ((Quantification) f).getF();

		}

		if (f instanceof Ou) {
			clauses.add((Ou) f);

		} else if (f instanceof Non) {
			clauses.add(f);

		} else if (f instanceof Atome) {
			clauses.add(f);

		} else if (f instanceof Et) {
			clauses.addAll(toClauses(((Et) f).getOperande(), nbCst));
			clauses.addAll(toClauses(((Et) f).getOperandedroit(), nbCst));
		}

		return clauses;

	}

	/**
	 * Renomme tout le terme d'une formule
	 * 
	 * @param f
	 *            la formule dont il faut renommer le terme
	 */
	public void renommer(Formule f) {

		// rename from the both sides of an OperandeBinaire
		if (f instanceof OperateurBinaire) {
			renommer(((OperateurBinaire) f).getOperande());
			renommer(((OperateurBinaire) f).getOperandedroit());

			// rename all under an OperandeUnaire
		} else if (f instanceof OperateurUnaire) {
			renommer(((OperateurUnaire) f).getOperande());

			// rename all the Terme of the Atome
		} else if (f instanceof Atome) {
			for (int i = 0; i < ((Atome) f).getArite(); i++) {
				renommer(((Atome) f).getOperandes());
			}
		}

	}

	/**
	 * Renomme tous les termes de la liste passée en paramètre
	 * 
	 * @param t
	 *            la liste de Terme à renomer
	 */
	public void renommer(Terme[] t) {

		for (int i = 0; i < t.length; i++) {
			renommer(t[i]);
		}

	}

	/**
	 * Renome le terme donné
	 * 
	 * @param t
	 *            le Terme à renommer
	 */
	public void renommer(Terme t) {

		// if it is a Fonction, so rename all is Variable
		if (t instanceof Fonction) {
			renommer(((Fonction) t).getOperandes());

			// if it is a variable, rename it by 'varRename' + a number
		} else if (t instanceof Variable) {

			// if the Variable has not already been renamed
			if (!t.getName().startsWith("varRename")) {

				Enumeration<Variable> vars = substitutionToClause.keys();
				while (vars.hasMoreElements()) {
					if (vars.nextElement().equals(((Variable) t).getName())) {
						return;
					}
				}

				// save all the Variable to rename
				substitutionToClause.put((Variable) t, new Variable("varRename" + changement));

			}

			// incremente the value of the renamed Variable
			changement++;
		}

	}

	/**
	 * A n'utiliser que dans l'unification (ne reste plus que des ou et des
	 * negations)
	 * 
	 * @param f
	 * @return
	 */
	public ArrayList<Formule> reccupererSousArray(Formule f) {
		ArrayList<Formule> clauses1 = new ArrayList<Formule>();
		if (f instanceof Ou) {
			clauses1 = ((Ou) f).reccupererAllAtomeNon();
		} else {

			clauses1.add(f);
		}

		return clauses1;
	}

	/**
	 * Permet de faire la substitution de la phase d'unification du processus
	 * 
	 * @param depart1
	 * @param depart2
	 * @param f1
	 *            le premier atome
	 * @param f2
	 *            le contraire de f1
	 * @return une ArrayList<Formule>
	 */
	public static ArrayList<Formule> substituer(ArrayList<Formule> depart1, ArrayList<Formule> depart2, Atome f1, Atome f2) {
		ArrayList<Formule> ret = new ArrayList<Formule>();

		// recherche des discordances si il n'y en a pas on retourne null
		// retourne null si il n'y a pas une variable a substituer
		// si les atomes ne sont pas de même non on ne peut pas substituer
		if (!f1.isTheSame(f2)) {
			return null;
		}

		Terme[] discordances = discordances(f1, f2);
		if (discordances == null || (discordances[0] instanceof Variable && discordances[1] instanceof Variable)) {
			// impossible a unifier
			return null;
		} else {
			if (discordances[0] instanceof Variable) {
				// si variable ok on peut substituer
				for (int i = 0; i < depart1.size(); i++) {
					depart1.get(i).substituer((Variable) discordances[0], discordances[1]);
				}

				for (int i = 0; i < depart2.size(); i++) {
					depart2.get(i).substituer((Variable) discordances[0], discordances[1]);
				}

				f1.substituer((Variable) discordances[0], discordances[1]);
				f2.substituer((Variable) discordances[0], discordances[1]);

			} else {
				for (int i = 0; i < depart1.size(); i++) {
					depart1.get(i).substituer((Variable) discordances[1], discordances[0]);
				}

				for (int i = 0; i < depart2.size(); i++) {
					depart2.get(i).substituer((Variable) discordances[1], discordances[0]);
				}

				f1.substituer((Variable) discordances[1], discordances[0]);
				f2.substituer((Variable) discordances[1], discordances[0]);

			}
			// suppression du terme definis
			// ssi les deux atomes sont egaux on peut enlever dans les formules
			if (f1.equals(f2)) {
				for (int i = 0; i < depart1.size(); i++) {
					if (depart1.get(i) instanceof Non) {
						if (f1.isTheSame((Atome) ((Non) depart1.get(i)).getOperande())) {
							depart1.remove(i);
						}
					} else {
						if (f1.isTheSame((Atome) depart1.get(i))) {
							depart1.remove(i);
						}
					}
				}

				for (int i = 0; i < depart2.size(); i++) {
					if (depart2.get(i) instanceof Non) {
						if (f2.equals((Atome) ((Non) depart2.get(i)).getOperande())) {
							depart2.remove(i);
						}
					} else {
						if (f2.equals((Atome) depart2.get(i))) {
							depart2.remove(i);
						}
					}
				}

				// verification au passage qu'il n' y a pas deux terme
				// identiques

				for (int i = 0; i < depart1.size(); i++) {
					for (int j = 0; j < depart2.size(); j++) {
						if (depart1.get(i).equals(depart2.get(j))) {
							// si il y en a deux identiques, on en garde plus
							// qu'un
							depart1.remove(i);

						} else {
							// si l'un et son contraire sont les même ont peux
							// les virés par unification A non(A)
							if (depart1.get(i).negation().equals(depart2.get(j))) {
								depart1.remove(i);
								depart2.remove(j);
							}
						}
					}
				}

				ret.addAll(depart1);
				ret.addAll(depart2);
			} else {
				return substituer(depart1, depart2, f1, f2);
			}
		}

		return ret;
	}

	/**
	 * Permet de voir s'il y a une discordance entre deux formules
	 * 
	 * @param t1
	 *            une Formule
	 * @param t2
	 *            une Formule
	 * @return la discordance des Formules, null sinon
	 */
	public static Terme[] discordances(Atome f1, Atome f2) {
		Terme[] termes1 = f1.getOperandes();
		Terme[] termes2 = f2.getOperandes();

		return discordances(termes1, termes2);
	}

	/**
	 * Permet de voir s'il y a une discordance entre plusieurs termes
	 * 
	 * @param t1
	 *            un tableau de Terme
	 * @param t2
	 *            un tableau de Terme
	 * @return la discordance des Termes , null sinon
	 */
	public static Terme[] discordances(Terme[] t1, Terme[] t2) {
		for (int i = 0; i < t1.length; i++) {
			for (int j = 0; j < t2.length; j++) {
				Terme[] disc = discordances(t1[i], t2[j]);
				if (disc != null) {
					return disc;
				}
			}
		}

		return null;
	}

	/**
	 * Permet de voir s'il y a une discordance entre deux termes
	 * 
	 * @param t1
	 *            un Terme
	 * @param t2
	 *            un Terme
	 * @return la discordance des Termes , null sinon
	 */
	public static Terme[] discordances(Terme t1, Terme t2) {
		if (t1 instanceof Fonction) {
			if (t2 instanceof Fonction) {
				if (t1.getName().equals(t2.getName())) {
					return discordances(((Fonction) t1).getOperandes(), ((Fonction) t2).getOperandes());
				}
			} else if (t2 instanceof Variable && !t1.contains((Variable) t2)) {
				Terme[] ret = new Terme[2];
				ret[0] = t1;
				ret[1] = t2;

				return ret;

			}
			return null;
		}

		if (t2 instanceof Fonction) {
			if (t1 instanceof Fonction) {
				if (t1.getName().equals(t2.getName())) {
					return discordances(((Fonction) t1).getOperandes(), ((Fonction) t2).getOperandes());
				}
			} else if (t1 instanceof Variable && !t2.contains((Variable) t1)) {
				Terme[] ret = new Terme[2];
				ret[0] = t1;
				ret[1] = t2;

				return ret;

			}
			return null;
		}

		if (((t1 instanceof Variable && t2 instanceof Variable) || (t1 instanceof Constante && t2 instanceof Constante)) || (t1.getName().equals(t2.getName()))) {
			return null;

		}

		Terme[] ret = new Terme[2];
		ret[0] = t1;
		ret[1] = t2;

		return ret;
	}

	/**
	 * Permet de savoir si une ArrayList<Formule> contient une Formule d'une
	 * autre ArrayList<Formule>
	 * 
	 * @param f1
	 *            une ArrayList<Formule>
	 * @param f2
	 *            l'ArrayList<Formule> pouvant contenir une formule de f1
	 * @return un boolean
	 */
	public static boolean theSame(ArrayList<Formule> f1, ArrayList<Formule> f2) {
		if (f1.size() != f2.size()) {
			return false;
		}

		for (Formule f : f1) {

			boolean ok = false;
			for (Formule ff2 : f2) {
				if (f.equals(ff2))
					ok = true;
			}
			if (ok == false) {
				return false;
			}
		}

		return true;
	}

	/**
	 * Permet de savoir si une ArrayList<Formule> contient une Formule d'une
	 * autre ArrayList<Formule> mais sous forme négative
	 * 
	 * @param f1
	 *            une ArrayList<Formule>
	 * @param f2
	 *            l'ArrayList<Formule> pouvant contenir une formule de f1 sous
	 *            forme négative
	 * @return un boolean
	 */
	public static boolean theSameNegative(ArrayList<Formule> f1, ArrayList<Formule> f2) {

		if (f1.size() != f2.size()) {
			return false;
		}

		for (Formule f : f1) {
			boolean ok = false;
			for (Formule ff2 : f2) {

				Formule ftemp = f.negation();

				if (ftemp.equals(ff2)) {

					ok = true;
				}
			}
			if (ok == false) {
				return false;
			}
		}

		return true;
	}

	/**
	 * Permet de savoir si une Arraylist<ArrayList<Formule>> contient une
	 * ArrayList<Formule>
	 * 
	 * @param f1
	 *            une ArrayList<ArrayList<Formule>>
	 * @param f2
	 *            une ArrayList<Formule>
	 * @return un boolan
	 */
	public boolean contains(ArrayList<ArrayList<Formule>> f1, ArrayList<Formule> f2) {

		for (ArrayList<Formule> list : f1) {
			if (theSame(list, f2))
				return true;
		}

		return false;
	}

	/**
	 * Permet de faire une copie d'une ArrayList<Formule>
	 * 
	 * @param f
	 *            une ArrayList<Formule>
	 * @return la copie de l'ArrayList<Formule> passé en paramêtre
	 */
	public static ArrayList<Formule> copy(ArrayList<Formule> f) {
		ArrayList<Formule> fcopy = new ArrayList<Formule>();
		for (int i = 0; i < f.size(); i++) {
			fcopy.add(f.get(i).copy());
		}

		return fcopy;
	}

}
